\subsection{General Properties}
\todo{Some properties that can be interesting to prove}

\begin{lemma}[Invariant Lemma]
 For each place $p \in P \setminus \{\Pclock\}$ if $p$ encodes a living resource then $M(p) = \tuple{1, n,m}$ and $n \geq m$, otherwise if $p$ represents a dead resource $M(p) = \tuple{0, n, 0}$. 
Moreover, for each place $p \in P $ $M'(p) = L_{\rho}(t,p)$.
\end{lemma}

\begin{theorem}[One Safe]
 The Petri net $P$ with initial marking $M_0$ is \emph{one safe}.
\end{theorem}

\begin{corollary}
 A place $p \in P \setminus \{\Pclock\}$ is either alive or dead never both.
\end{corollary}


\subsection{Preliminaries on Well Structured Transition Systems}
The decidability of reachability for Petri Nets with Timestamps will be shown by appealing to the theory of
well-structured transition systems \cite{FinkelS01,AbdullaCJT00}.
The following results and definitions are from \cite{FinkelS01},  unless
differently specified. 

Recall that a \emph{quasi-order} (or, equivalently, preorder) is a reflexive
and transitive relation.

\begin{definition}[Well-quasi-order]
A \emph{well-quasi-order} (wqo) is a quasi-order $\leq$ over a
set $X$ such that, for any infinite sequence $x_0 , x_1 , x_2 \ldots \in X$, there exist indexes $i < j$
such that $x_i \leq x_j$.
\end{definition}

 Note that if $\leq$ is a wqo then any infinite sequence $x_0 , x_1 , x_2 , \ldots$ contains an infinite
increasing subsequence $x_{i_0} , x_{i_1} , x_{i_2} , \ldots$ (with $i_0 < i_1 < i_2 < \ldots$). 
Thus well-quasi-orders exclude the possibility of having infinite strictly decreasing sequences.


Here and in the following %$\rightarrow^{+}$ (resp. 
$\rightarrow^*$ denotes the 
%transitive (resp. the 
reflexive and transitive
%) 
closure of the relation $\rightarrow$.


\begin{definition}[Transition system]
\label{def:WSTS}
A \emph{transition system} is a structure $TS = (S, \rightarrow)$, where $S$ is a set of states
and $\rightarrow \subseteq  S \times S$ is a set of transitions. 
We define $Succ(s)$ as the set $\{s' \in S \mid s \rightarrow s' \}$
of immediate \emph{successors} of $s$. %We say that 
$TS$ is \emph{finitely branching} if, for each $s \in S$,
$Succ(s)$ is finite.
We also define $Pred(s)$ as the set $\{s' \in S \mid s' \rightarrow s\}$ of \emph{immediate predecessors} of $s$,
while $Pred^*(s)$ and $Pred^+(s)$ denote the sets $\{s \in S \mid s' \rightarrow^* s\}$ and  $\{s \in S \mid s' \rightarrow^+ s\}$, respectively, of \emph{predecessors} of $s$.
\end{definition}

\begin{newnotation}
In the rest of the paper, 
and with a slight abuse of notation,
we will  assume the expected point-wise extensions of definitions to sets. 
For instance, 
function $Succ$ just defined on states is extended to sets of states as:
 %, $Pred$, $Pred^*$ and  $Pred^+$
%will also be used  
%on sets, %by assuming 
%that in this case they are defined by 
%the point-wise extension of the above definitions, 
$Succ(S) = \bigcup_{s \in S} Succ(s)$.  
\end{newnotation}




The key tool to 
the decidability of 
%decide 
several properties of computations 
is the notion of \emph{well-structured transition system} \cite{FinkelS01,AbdullaCJT00}. 
This is a transition system equipped with a well-quasi-order on states
which is (upward) compatible with the transition relation. Here we will use a strong version 
of compatibility; hence the following definition.


\begin{definition}[Well-structured transition system] %with strong compatibility]
A \emph{well-struc\-tured transition system with strong compatibility} is a transition system 
$TS = (S, \rightarrow)$, equipped with a quasi-order $\leq$ on $S$, such that the two following conditions hold:
%\vspace{-2mm}
\begin{enumerate}
\item 
 $\leq$ is a well-quasi-order;
\item 
 $\leq$ is strongly (upward) compatible with $\rightarrow$, that is, for all $s_1 \leq t_1$ and all transitions
   $s_1 \rightarrow s_2$ , there exists a state $t_2$ such that $t_1 \rightarrow t_2$ and $s_2 \leq t_2$ holds.
\end{enumerate}
\end{definition}

The following theorem is a special case of Theorem 4.6 in \cite{FinkelS01} and will be used to obtain our decidability result.

\begin{theorem}\label{th:Finkel}
Let $TS = (S, \rightarrow, \leq)$ be a finitely branching, well-structured transition
system with strong compatibility, decidable $\leq$,  and computable $Succ$. Then the existence
of an infinite computation starting from a state $s \in S$ is decidable.
\end{theorem}

Given a quasi-order $\leq$ over $X$, an {\em upward-closed set} is a subset $I\subseteq X$ such that
the following holds: $\forall x,y\in X: (x\in I\wedge x\leq y)\Rightarrow y\in I$. Given $x\in X$, we define its upward closure as $\uparrow x = \{y\in X\mid x\leq y\}$. This notion can be extended to sets as expected: given a set $Y\subseteq X$ we define its upward closure as $\uparrow Y = \bigcup_{y\in Y}\uparrow y$. 

\begin{definition}[Finite basis]\label{d:finbas}
A {\em finite basis} of an upward-closed set $I$ is a finite set $B$ such that $I = \bigcup_{x\in B}\uparrow x$.
\end{definition}

%In our case t
The notion of basis is particularly important when considering 
the basis of the predecessor of a state in a transition system. More precisely, we are interested in  \emph{effective} pred-basis as defined below.

\begin{definition}[Effective pred-basis]\label{d:efpb}
A well-structured transition system has {\em effective pred-basis} if there exists an algorithm such that, for any state $s\in S$, it returns the set $pb(s)$ which is a finite basis of $\uparrow Pred(\uparrow s)$.
\end{definition}

The following proposition is a special case of Proposition 3.5 
in \cite{FinkelS01}.
\begin{proposition} \label{predcomp}
Let $TS = (S,\rightarrow,\leq)$ be a finitely branching,
well-structured transition system
with strong compatibility, decidable $\leq$ and effective pred-basis.
It is possible to compute a finite basis of $Pred^*(I)$ for any upward-closed set $I$
given via a finite basis.
\end{proposition}

% We will also need a result due to Higman \cite{Higman52} which allows to extend a well-quasi-order
% from a set $S$ to the set of the finite sequences on $S$. More precisely, given a set $S$ let
% us denote by $S^*$ the set of finite sequences built by using elements in $S$. 
% We can define a quasi-order on $S^*$ as follows.
% 
% \begin{definition}\label{def:eqwqo}
% Let $S$ be a set and $\leq$ a quasi-order over $S$. The relation $\leq_*$ over $S^*$
% is defined as follows. Let $t, u \in S^*$, with $t = t_1 t_2 \ldots t_m$ and $u = u_1 u_2 \ldots u_n$. 
% We have that $t \leq_* u$ if and only if there exists an injection $f$ from $\{1, 2, \ldots m \}$ 
% to $\{1, 2, \ldots n\}$ such that $t_i \leq u_{f (i)}$ and $f(i) < f(i+1)$ 
% for $i = 1, \ldots , m-1$.
% \end{definition}
% 
% The relation $\leq_*$ is clearly a quasi-order over $S^*$. 
% It is also a wqo, since we have the following result.
% 
% \begin{lemma}[Higman] %\cite{Higman52}] 
% \label{lem:Higman}
% Let $S$ be a set and $\leq$ a wqo over $S$. 
% Then %the relation 
% $\leq_*$ is a wqo over $S^*$.
% \end{lemma}

Finally we will use the following proposition, whose proof is immediate.

\begin{proposition}\label{prop:eqwqo}
Let $S$ be a finite set. Then the equality is a wqo over $S$.
\end{proposition}


% %Another 
% %An extension to the theory of wqo is needed in the rest of the paper. 
% We shall also appeal to the following result.
% In \cite{kruskal60}, Kruskal proved that a wqo on a set $S$ can be extended to the set of finite trees whose nodes have labels ranging in $S$; we refer to this as the set of trees \emph{over} $S$.
% We first define how to extend a quasi order on a set $S$ to the trees over $S$.
% If $t$ is a tree and $n$ a node in $t$, we denote with $label(n)$ the label of the node $n$.
% 
% \begin{definition}\label{def:prectr}
%   Let $S$ and $\leq$ be a set and a wqo over $S$, respectively. 
%   The relation $\leq^{\mathsf{tr}}$ on the set of
% trees over $S$ is defined as follows. Let $t, u$ be trees over $S$. We have that $t \leq^{\mathsf{tr}} u$ iff there
% exists an injection $f$ from the nodes of $t$ to the ones of $u$ such that:
% \begin{enumerate}
%  \item Let $m,n$ be nodes in $t$. If $m$ is an ancestor of $n$ then $f(m)$ is an ancestor of $f(n)$.
%  \item Let $m,n,p$ be nodes in $t$. If $p$ is the minimal common ancestor of $m$ and $n$ then $f(p)$ is the minimal common ancestor of $f(m)$ and $f(n)$.
%  \item Let $n$ be a node in $t$. Then $label(n) \leq label(f(n))$.
% \end{enumerate}
% \end{definition}
% 
% %Similarly as before t
% The relation $\leq^{tr}$ is  a quasi-order over the trees over $S$. 
% It is also a wqo, since we have the following result.
% 
% \begin{theorem}[Kruskal \cite{kruskal60}]\label{lem:kruskal}
%    Let $S$ be a set and $\leq$ a wqo over $S$. Then, the relation $\leq^{tr}$ 
% is a wqo on the set of trees over $S$.
% \end{theorem}
% 
% 

% 



\subsection{Reachability is decidable}
